proof: WfCNF wrap of the RankMonoUnion umbrella by hyperpolymath · Pull Request #169 · hyperpolymath/echo-types

hyperpolymath · 2026-05-30T14:48:05Z

Summary

Stacked on #168. Mirrors `RankMonoUmbrellaSlice4.<ᵇ⁻ⁿ`'s WfCNF-bundling pattern over `RankMonoUnion.<ᵇᵘ` from #168. Provides the canonical-form invariant downstream Buchholz consumers need alongside the rank-relation. Zero new proof obligations; `--safe --without-K`, no postulates, no funext.

What ships

Name	Type	Role
`<ᵇᵘⁿ`	record (WfCNF + WfCNF + `<ᵇᵘ`)	WfCNF-narrowed union relation
`mk<ᵇᵘⁿ`	record constructor	Bundling combinator
`<ᵇᵘⁿ-from-<ᵇ⁰` / `<ᵇᵘⁿ-from-<ᵇ¹` / `<ᵇᵘⁿ-from-<ᵇ⁺²`	embeddings	Constructor-level uplifts under WfCNF endpoints
`rank-pow-mono-<ᵇᵘⁿ`	rank-mono theorem	One-liner forwarding through bundled `<ᵇᵘ-d`

Architectural payoff preserved

The "union of extensions" pattern from #168 extends through the WfCNF wrap automatically. Future contributors adding a new source-rule extension `<ᵇⁿ`:

Edit `RankMonoUnion` to extend `<ᵇᵘ` with the new disjunct + `rank-pow-mono-<ᵇᵘ` with the new case.
This module updates AUTOMATICALLY — no edit needed.

Per-extension proof work + structural composition. No proof obligations multiply across the WfCNF boundary either.

Slice 3+4 Route A session arc (5 PRs)

PR	Layer
#165	rank-lex-jb (b) primitive
#166	rank-lex-jb (c) trichotomy + first-eq
#167	Path-3 prototype (same-left source-rule extension)
#168	RankMonoUnion (architecture)
THIS PR	WfCNF wrap of the union

Local verification

All four Agda lanes typecheck clean, exit 0.
`bash tools/check-guardrails.sh proofs/agda` — 163 modules pass.
`sh scripts/kernel-guard.sh` — PASS.

Six new names pinned in `Ordinal/Buchholz/Smoke.agda`.

Test plan

Module typechecks under `--safe --without-K` with zero postulates.
Full suite + Smoke remain green with the new module wired in.
CI: `check` + `cold-check` + governance lanes green.
Auto-merge on green AFTER proof(architecture): RankMonoUnion umbrella over source-rule extensions #168 merges (stacked).

🤖 Generated with Claude Code

## Summary **Closes Gate 2 of the Slice 3+4 Route A session arc.** Derives \`WellFounded _<ᵇᵘ_\` mechanically from \`rank-pow-mono-<ᵇᵘ\` (#168) and the existing \`wf-<′\` via the standard Subrelation + InverseImage transport pattern documented in \`Ordinal.Buchholz.RankBrouwer\`'s preamble. **Zero new proof obligations**; purely structural. \`--safe --without-K\`, no postulates, no funext. ## The rank-embedding recipe ```agda wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y) wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′ wf-<ᵇᵘ : WellFounded _<ᵇᵘ_ wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback ``` Two steps: 1. \`On.wellFounded\` (= \`InverseImage.wellFounded\`) lifts well-foundedness of \`_<′_\` on \`Ord\` to the pullback \`_<′_ on rank-pow\` on \`BT\`. 2. \`Subrelation.wellFounded\` transports well-foundedness from the pullback to \`_<ᵇᵘ_\`, consuming \`rank-pow-mono-<ᵇᵘ\` as the witness that \`_<ᵇᵘ_\` is a sub-relation of the pullback. The pattern is documented at \`RankBrouwer.agda:55-56\`. ## Slice 3+4 Route A gate status after this PR | Gate | Status | |---|---| | 1 — tail-rank-equality discharge (cross-head rank-equal case) | open (structural blocker) | | **2 — well-foundedness of \`_<ᵇᵘ_\`** | **CLOSED HERE** | | 3 — Path-4 + further source-rule extensions | open (future-work, mechanical) | ## What this does NOT do - Does NOT prove well-foundedness of the WfCNF-narrowed \`_<ᵇᵘⁿ_\` (#169) separately — follows by the same Subrelation transport from \`wf-<ᵇᵘ\` via the canonical \`<ᵇᵘⁿ → <ᵇᵘ\` projection. Left for a thin follow-on if specifically needed. - Does NOT add a Brouwer-rank embedding stronger than \`rank-pow\` — \`rank-pow\` is K-free + lands in \`Ord\` + already discharges the WF transport. ## Local verification - All four Agda lanes typecheck clean, exit 0. - \`bash tools/check-guardrails.sh proofs/agda\` — 163 modules pass. - \`sh scripts/kernel-guard.sh\` — PASS. Two new names pinned in \`Ordinal/Buchholz/Smoke.agda\`: \`wf-rank-pow-pullback\`, \`wf-<ᵇᵘ\`. ## Slice 3+4 Route A session arc (6 PRs) | PR | Layer | |---|---| | #165 | rank-lex-jb (b) primitive | | #166 | rank-lex-jb (c) trichotomy + first-eq | | #167 | Path-3 same-left source-rule extension | | #168 | RankMonoUnion architecture | | #169 | WfCNF wrap of the union | | **THIS PR** | **WF of the union (Gate 2 closure)** | ## Test plan - [x] Module typechecks under \`--safe --without-K\` with zero postulates. - [x] Full suite + Smoke remain green with the new module wired in. - [ ] CI: \`check\` + \`cold-check\` + governance lanes green. - [ ] Auto-merge on green. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Mirrors `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`'s WfCNF-bundling pattern over `RankMonoUnion._<ᵇᵘ_` (PR #168). Provides the canonical-form invariant downstream Buchholz consumers need alongside the rank- relation. Zero new proof obligations; the rank-mono closure forwards through the bundled `_<ᵇᵘ_` derivation. `--safe --without-K`, no postulates, no funext. `record _<ᵇᵘⁿ_ (x y : BT) : Set` bundling: * `wf-x : WfCNF x` — source-side canonical-form witness * `wf-y : WfCNF y` — target-side canonical-form witness * `<ᵇᵘ-d : x <ᵇᵘ y` — the union derivation from `RankMonoUnion` Three constructor-level embeddings: `<ᵇᵘⁿ-from-<ᵇ⁰` (10 inherited cases), `<ᵇᵘⁿ-from-<ᵇ¹` (Slice 3 strict-head joint- bplus), `<ᵇᵘⁿ-from-<ᵇ⁺²` (Path-3 same-left joint-bplus). `rank-pow-mono-<ᵇᵘⁿ : ∀ {x y} → x <ᵇᵘⁿ y → rank-pow x <′ rank-pow y` forwards directly to `rank-pow-mono-<ᵇᵘ` via the bundled derivation. ONE LINE — same shape as Slice 4's `rank-pow-mono-<ᵇ⁻ⁿ`. The "union of extensions" pattern from #168 extends through the WfCNF wrap automatically. Future contributors adding a new source-rule extension `_<ᵇⁿ_`: 1. Edit `RankMonoUnion` to extend `_<ᵇᵘ_` with the new disjunct + `rank-pow-mono-<ᵇᵘ` with the new case. 2. THIS MODULE updates AUTOMATICALLY — no edit needed. Per-extension proof work + structural composition; no proof obligations multiply across the WfCNF boundary either. - All four Agda lanes typecheck clean, exit 0. - `bash tools/check-guardrails.sh proofs/agda` — **163 modules** pass. - `sh scripts/kernel-guard.sh` — PASS. Six new names pinned in `Ordinal/Buchholz/Smoke.agda`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-30T15:28:13Z

🔍 Hypatia Security Scan

Findings: 58 issues detected

Severity	Count
🔴 Critical	17
🟠 High	22
🟡 Medium	19

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "unknown",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

hyperpolymath changed the base branch from session/rank-mono-union-umbrella to main May 30, 2026 14:48

hyperpolymath enabled auto-merge (squash) May 30, 2026 14:48

hyperpolymath mentioned this pull request May 30, 2026

proof: well-foundedness of _<ᵇᵘ_ via rank-embedding transport #170

Merged

4 tasks

hyperpolymath force-pushed the session/rank-mono-union-wfcnf branch from de1d789 to 59beaab Compare May 30, 2026 15:18

hyperpolymath merged commit ed347df into main May 30, 2026
10 of 12 checks passed

hyperpolymath deleted the session/rank-mono-union-wfcnf branch May 30, 2026 15:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof: WfCNF wrap of the RankMonoUnion umbrella#169

proof: WfCNF wrap of the RankMonoUnion umbrella#169
hyperpolymath merged 1 commit into
mainfrom
session/rank-mono-union-wfcnf

hyperpolymath commented May 30, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 30, 2026

Summary

What ships

Architectural payoff preserved

Slice 3+4 Route A session arc (5 PRs)

Local verification

Test plan

Uh oh!

Uh oh!

github-actions Bot commented May 30, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant